EquivRel(;A,B.A  B) 

latex

ProofTree

Definitions	EquivRel(T;x,y.E(x;y)), P  Q, P  Q, x:A. B(x), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), P  Q, Refl(T;x,y.E(x;y)), P & Q, t  T,
Lemmas	iff wf